es:event_system{i:l}, e:es-E(es).
((es-first(es; e)))  sqequal(es-init(es;e); es-init(es;es-pred(es; e))) 

latex

Definitions	False, P  Q, A, x:AB(x), x:A. B(x), b, x:A  B(x), P  Q, P  Q, , s = t, t  T, Unit, left + right, es-init(es;e), es-E(es), event_system{i:l}
Lemmas	do-apply-pred?, eqtt to assert, iff transitivity, eqff to assert, can-apply-pred?, not functionality wrt iff, assert of bnot